(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 9))
(let ((e4 (* v1 v2)))
(let ((e5 (- e4 v1)))
(let ((e6 (+ v1 e5)))
(let ((e7 (- v2 e6)))
(let ((e8 (/ e3 e3)))
(let ((e9 (* e6 e3)))
(let ((e10 (- e4 e5)))
(let ((e11 (- e9 e10)))
(let ((e12 (* (- e3) v1)))
(let ((e13 (+ e6 e10)))
(let ((e14 (/ e3 e3)))
(let ((e15 (/ e3 (- e3))))
(let ((e16 (+ e5 e15)))
(let ((e17 (+ e7 e12)))
(let ((e18 (- e14 v0)))
(let ((e19 (> e10 e16)))
(let ((e20 (<= e5 e11)))
(let ((e21 (<= v2 v0)))
(let ((e22 (< v2 v0)))
(let ((e23 (< e6 e15)))
(let ((e24 (= v0 e10)))
(let ((e25 (> e15 e10)))
(let ((e26 (> v2 e9)))
(let ((e27 (<= v0 e15)))
(let ((e28 (distinct e5 e8)))
(let ((e29 (= e18 e7)))
(let ((e30 (> e17 e12)))
(let ((e31 (distinct e7 e8)))
(let ((e32 (< e10 e12)))
(let ((e33 (> e18 e17)))
(let ((e34 (<= v0 e4)))
(let ((e35 (< v1 e4)))
(let ((e36 (> e5 e7)))
(let ((e37 (<= e13 e10)))
(let ((e38 (= e10 e14)))
(let ((e39 (= e14 e8)))
(let ((e40 (> e9 e8)))
(let ((e41 (< e17 e13)))
(let ((e42 (distinct v2 v0)))
(let ((e43 (<= v0 e15)))
(let ((e44 (<= e11 e6)))
(let ((e45 (= e5 e9)))
(let ((e46 (>= e4 e5)))
(let ((e47 (> e13 e17)))
(let ((e48 (< v1 e5)))
(let ((e49 (>= e8 e9)))
(let ((e50 (distinct e16 e11)))
(let ((e51 (< e12 e9)))
(let ((e52 (> v1 e6)))
(let ((e53 (= v0 e14)))
(let ((e54 (>= e17 e4)))
(let ((e55 (= e6 e10)))
(let ((e56 (<= e6 e9)))
(let ((e57 (<= e5 e11)))
(let ((e58 (= e7 v0)))
(let ((e59 (distinct e17 e9)))
(let ((e60 (> e4 e14)))
(let ((e61 (< e12 e17)))
(let ((e62 (< e12 e6)))
(let ((e63 (>= e7 e16)))
(let ((e64 (<= e4 e15)))
(let ((e65 (>= e17 e6)))
(let ((e66 (= e5 e10)))
(let ((e67 (= e9 e16)))
(let ((e68 (distinct e18 e16)))
(let ((e69 (or e41 e56)))
(let ((e70 (= e49 e45)))
(let ((e71 (ite e48 e27 e48)))
(let ((e72 (xor e28 e58)))
(let ((e73 (=> e31 e62)))
(let ((e74 (ite e73 e19 e59)))
(let ((e75 (not e43)))
(let ((e76 (ite e60 e72 e23)))
(let ((e77 (or e54 e33)))
(let ((e78 (=> e37 e63)))
(let ((e79 (not e40)))
(let ((e80 (= e42 e42)))
(let ((e81 (ite e46 e22 e26)))
(let ((e82 (and e39 e77)))
(let ((e83 (= e68 e79)))
(let ((e84 (xor e38 e65)))
(let ((e85 (ite e69 e29 e61)))
(let ((e86 (ite e34 e30 e47)))
(let ((e87 (ite e52 e67 e86)))
(let ((e88 (ite e81 e44 e55)))
(let ((e89 (not e50)))
(let ((e90 (and e64 e66)))
(let ((e91 (or e80 e70)))
(let ((e92 (not e57)))
(let ((e93 (=> e76 e71)))
(let ((e94 (= e25 e88)))
(let ((e95 (and e51 e94)))
(let ((e96 (not e84)))
(let ((e97 (=> e36 e24)))
(let ((e98 (not e20)))
(let ((e99 (xor e78 e95)))
(let ((e100 (xor e93 e93)))
(let ((e101 (=> e98 e92)))
(let ((e102 (not e53)))
(let ((e103 (not e101)))
(let ((e104 (or e96 e90)))
(let ((e105 (=> e87 e89)))
(let ((e106 (xor e103 e75)))
(let ((e107 (and e74 e102)))
(let ((e108 (ite e99 e35 e99)))
(let ((e109 (=> e108 e105)))
(let ((e110 (ite e83 e100 e107)))
(let ((e111 (and e85 e110)))
(let ((e112 (and e91 e106)))
(let ((e113 (or e104 e104)))
(let ((e114 (= e113 e112)))
(let ((e115 (and e32 e21)))
(let ((e116 (not e114)))
(let ((e117 (= e116 e116)))
(let ((e118 (and e97 e117)))
(let ((e119 (ite e115 e115 e118)))
(let ((e120 (not e111)))
(let ((e121 (or e82 e82)))
(let ((e122 (xor e121 e119)))
(let ((e123 (ite e120 e122 e109)))
e123
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
